Non puoi farlo perchè non è implementato il for All (e nel codice viene usato quello per fare model checking CTL)